Uma Lógica para a Referência Ambígua
by Andressa Sebben and Arthur Buchsbaum

XXXIII Conferência Latinoamericana de Informática, San José,Costa Rica, 2007

Abstract: This work presents a description logic named LAR – Logic of Ambiguous Reference – aiming to formalize suitably situations of ambiguity and vacuity arising in natural languages and, implicitly, in mathematical discourse. A language for it is described, together with a semantics and a sequent calculus. Some syntactic results and a theorem of elimination of descriptions are also provided.

Download (100 Kbytes)

Um Método dos Tableaux com um Refinamento para Evitar Repetições Desnecessárias de Fórmulas Universais nos Ramos das Árvores de Prova,
by Leticia Carvalho Pivetta Fendt and Arthur Buchsbaum

V Encontro Nacional de Inteligência Artificial, Brazil, 2005, pp. 801-810.
Internet: http://www.unisinos.br/_diversos/congresso/sbc2005/_dados/anais/pdf/arq0124.pdf.

Abstract: An enhancement of tableau method, non based on unification, aiming to diminish the number of nodes in proof trees and to increase probability of acquiring answers for a great number of questions. An algorithm, based on traditional tableau method for classical logic, uses an additional routine for controlling repetition of universal formulas in a given branch.

Download (476 Kbytes)

Um Método de Tableaux por Prova Direta para a Lógica Proposicional Clássica,
by Arthur Buchsbaum and Maurício Correia Lemes Neto

XI Escola Regional de Informática, 2003, Londrina, Paraná, Brazil, pp. 14-22.

Abstract: A tableau method for classical propositional logic, in which the proof tree is developed from the original formula given as a possible conclusion of inference, instead of its negation, as it is done usually by refutation proofs.

A Logic for Ambiguous Description,
by Arthur Buchsbaum

9th Workshop on Logic, Language, Information and Computation, Rio de Janeiro, Brazil, 2002, pp. 149-166.

Abstract: A logic formalizing ambiguity, which appears both in natural language and in mathematical discourse, is presented, through a sequent calculus and a semantics, together with some elementary results.

Download (234 Kbytes)

Um Método dos Tableaux para evitar Repetições de Fórmulas nos Ramos das Árvores de Prova,
by Arthur Buchsbaum and Leticia Carvalho Pivetta Fendt

I Congresso de Informática de Rondônia, Proceedings of I CONINFO-RO, 2002, Ji-Paraná, Rondônia, Brazil, pp. 1-10

Abstract: An enhancement of tableau method, non based on unification, aiming to diminish the number of nodes in proof trees and to increase probability of acquiring answers for a great number of questions. An algorithm, based on traditional tableau method for classical logic, uses an additional routine for controlling repetition of universal formulas in a given branch.

A Positive Formalization for the Notion of Pragmatic Truth,
by Arthur Buchsbaum, Tarcisio Pequeno and Marcelino Pequeno

International Conference on Artificial Intelligence, 2001, Las Vegas, Nevada, USA, v. II, pp. 902-908.
Internet: http://www.lip.uns.edu.ar/cmsra/pequeno-t.pdf.

Abstract: A logic of pragmatic truth is presented, aiming to overcome some problems of a previous formalization by Newton C. A. da Costa and collaborators, which assigns a central role to logical possibility. It is argued that not being in conflict with assumed knowledge is not enough for considering true a proposition, that is only a necessary condition. A typical picture of the way a scientific theory evolves exhibit alternative hypotheses competing for expanding a theory. A pragmatic knowledge, in this stage of theory development, is one that can be considered true in face of all alternative hypotheses. The logic presented here formalizes this process of knowledge evolution.

Download (108 Kbytes)

O Método dos Tableaux com Unificação,
by Arthur Buchsbaum and Leticia Carvalho Pivetta Fendt

III Encontro Nacional de Inteligência Artificial, 2001, Fortaleza, Ceará, Brazil.

Abstract: An enhancement of traditional tableau method, aiming to diminish the number of nodes of proof trees, and to increase probability of acquiring answers, based on unification procedure, commonly used in resolution method.

Download (80 Kbytes)

Abstract: Three basic alternatives to classical negation, represented by paraconsistent calculus C₁, the paracomplete calculus P₁, and the non alethic calculus N₁, all defined by Newton C. A. da Costa. For each of these calculi it is provided a corresponding tableau system. A general proof of correctness and completeness is given, including as special cases these three systems.

Download (89 Kbytes)

Abstract: A proof method based on tableaux for a subset of the Logic of Epistemic Inconsistency, suitable as a basis for automatizing a logic of defaults.

Abstract: A proof method based on tableaux for a subset of the Logic of Epistemic Inconsistency, suitable as a basis for automatizing a logic of defaults.

Abstract: It is introduced the idea of epistemic inconsistency, referring to contradictory viewpoints about a same situation. Such contradictions don't reflect an anomalous behavior of state of affairs, but incompleteness or vagueness of our knowledge about it. Association of this phenomenon with non monotonic reasoning is discussed. A logic, its calculus and semantics, aiming to precise this notion and to represent reasoning about contradictory views, without implying triviality, is presented.

Download (138 Kbytes)

Abstract: Tableau systems for a family of paraconsistent and/or paracomplete logics defined by Newton C. A. da Costa.

Download (78 Kbytes)

Abstract: An automated proof method for a paraconsistent logic, the calculus C₁* of Newton C. A. da Costa. Actually two tableau systems were constructed: one with a small number of rules, from which the correctness and completeness of the method was proved, and other one, equivalent to the former, is a system of derived rules, which was implemented.

Uma Lógica para a Referência Ambígua
de Andressa Sebben e Arthur Buchsbaum

XXXIII Conferência Latinoamericana de Informática, San José, Costa Rica, 2007.

Resumo: Este trabalho apresenta uma lógica descritiva denominada LAR – Lógica da Referência Ambígua – visando formalizar adequadamente situações de ambiguidade e vacuidade presentes nas linguagens naturais e, implicitamente, no discurso matemático. Uma linguagem para a mesma é descrita, juntamente com uma semântica e um cálculo de sequentes. Alguns resultados sintáticos e um teorema de eliminação das descrições são também apresentados.

Baixar (100 Kbytes)

Um Método dos Tableaux com um Refinamento para Evitar Repetições Desnecessárias de Fórmulas Universais nos Ramos das Árvores de Prova,
de Leticia Carvalho Pivetta Fendt e Arthur Buchsbaum

V Encontro Nacional de Inteligência Artificial, 2005, pgs. 801-810.
Internet: http://www.unisinos.br/_diversos/congresso/sbc2005/_dados/anais/pdf/arq0124.pdf.

Resumo: Um refinamento ao método dos tableaux, não baseado em unificação, visando diminuir o número de nós das árvores de prova e aumentar a probabilidade de obtenção de respostas para um número maior de problemas. Um algoritmo, baseado no método tradicional dos tableaux para a lógica clássica, recorre a uma rotina adicional para controlar a repetição de fórmulas universais em um dado ramo.

Baixar (476 Kbytes)

Um Método de Tableaux por Prova Direta para a Lógica Proposicional Clássica,
de Arthur Buchsbaum e Maurício Correia Lemes Neto

XI Escola Regional de Informática, 2003, Londrina, Paraná, pgs. 14-22.

Resumo: Um método de tableaux para a Lógica Proposicional Clássica, no qual a árvore de prova é desenvolvida a partir da própria fórmula dada como possível conclusão da inferência, ao invés de sua negação, como é feito tradicionalmente em provas por refutação.

A Logic for Ambiguous Description,
de Arthur Buchsbaum

9th Workshop on Logic, Language, Information and Computation, Rio de Janeiro, 2002, pgs. 149-166.

Resumo: Uma lógica que formaliza a ambigüidade, a qual está presente tanto na linguagem natural como no discurso matemático, é apresentada, através de um cálculo de seqüentes e de uma semântica, juntamente com alguns resultados elementares.

Baixar (234 Kbytes)

Um Método dos Tableaux para evitar Repetições de Fórmulas nos Ramos das Árvores de Prova,
de Arthur Buchsbaum e Leticia Carvalho Pivetta Fendt

I Congresso de Informática de Rondônia, Anais do I CONINFO-RO, 2002, Ji-Paraná, Rondônia, pgs. 1-10

Resumo: Um refinamento ao método dos tableaux, não baseado em unificação, visando diminuir o número de nós das árvores de prova e aumentar a probabilidade de obtenção de respostas para um número maior de problemas. Um algoritmo, baseado no método tradicional dos tableaux para a lógica clássica, recorre a uma rotina adicional para controlar a repetição de fórmulas universais em um dado ramo.

A Positive Formalization for the Notion of Pragmatic Truth,
de Arthur Buchsbaum, Tarcisio Pequeno e Marcelino Pequeno

International Conference on Artificial Intelligence, 2001, Las Vegas, Nevada, EUA, v. II, pgs. 902-908.
Internet: http://www.lip.uns.edu.ar/cmsra/pequeno-t.pdf.

Resumo: Uma lógica da verdade pragmática buscando superar problemas de uma formalização prévia apresentada por Newton C. A. da Costa e colaboradores, a qual atribui um papel central à possibilidade lógica. É argüido que não estar em conflito com o conhecimento assumido não é suficiente para considerar uma proposição como verdadeira; isto é apenas uma condição necessária. Um quadro típico do modo pelo qual uma teoria científica evolui exibe hipóteses alternativas competindo para expandir a teoria. Um conhecimento pragmático, neste estágio de desenvolvimento da teoria, é aquele que pode ser considerado verdadeiro diante de todas as hipóteses alternativas. A lógica aqui apresentada formaliza este processo de evolução do conhecimento.

Baixar (108 Kbytes)

O Método dos Tableaux com Unificação,
de Arthur Buchsbaum e Leticia Carvalho Pivetta Fendt

III Encontro Nacional de Inteligência Artificial, 2001, Fortaleza, Ceará.

Resumo: Um refinamento sobre o método dos tableaux, tal como tradicionalmente apresentado, visando diminuir o número de nós das árvores de prova, bem como aumentar a possibilidade de obtenção de respostas, baseado no procedimento de unificação, comumente utilizado no método da resolução.

Baixar (80 Kbytes)

Resumo: Três alternativas básicas à negação clássica, representadas pelo cálculo paraconsistente C₁, o cálculo paracompleto P₁, e o cálculo não alético N₁, todos definidos por Newton C. A. da Costa. Para cada um destes cálculos é dado um sistema de tableaux correspondente. É exposta uma prova geral de correção e completude, incluindo como casos particulares estes três sistemas.

Baixar (89 Kbytes)

Resumo: Um método de prova baseado em tableaux para um subconjunto da Lógica da Inconsistência Epistêmica, adequado como base para uma automatização de uma lógica de defaults.

Resumo: Um método automático de prova baseado em tableaux para um subconjunto da Lógica da Inconsistência Epistêmica, adequado como base para uma automatização de uma lógica de defaults.

Resumo: A noção de inconsistência epistêmica, referindo-se a visões contraditórias sobre uma mesma situação, é introduzida. Tais contradições não refletem um comportamento anômalo do estado das coisas, mas sim a incompletude ou vagueza de nosso conhecimento acerca deste. A associação deste fenômeno com o raciocínio não monotônico é debatida. Uma lógica, o seu cálculo e semântica, visando tornar precisa esta noção e viabilizar o raciocínio envolvendo visões contraditórias, sem acarretar trivialidade, é apresentada.

Baixar (138 Kbytes)

Resumo: Sistemas de tableaux para uma família de lógicas paraconsistentes e/ou paracompletas definidas por Newton C. A. da Costa.

Baixar (78 Kbytes)

Resumo: Um método de prova automático para uma lógica paraconsistente, o cálculo C₁* de Newton C. A. da Costa, é apresentado. Trata-se de um método analítico utilizando um sistema de tableaux. Na realidade, dois sistemas de tableaux foram elaborados: um com um número pequeno de regras, a partir do qual são provadas a consistência e a completude do método, e outro, que mostramos ser equivalente ao primeiro, é um sistema de regras derivadas a partir do qual foi realizada uma implementação. Este artigo apresenta a minha dissertação de mestrado de uma forma concisa.